Nuprl Lemma : subtype-fpf-variant
11,40
postcript
pdf
A
:Type{i},
P
:(
A
{i}),
B
:(
A
Type{i'}).
a
:{
a
:
A
|
P
(
a
)} fp
B
(
a
)
r
a
:
A
fp
B
(
a
)
latex
Definitions
parm{i}
Lemmas
subtype-fpf-general
origin
A:Type{i}, P:(A
{i}), B:(AType{i'}). a:{a:A| P(a)} fp B(a) 
r a:A fp B(a) A:Type{i}, P:(A{i}), B:(AType{i'}). a:{a:A| P(a)} fp B(a) r a:A fp B(a)